Nuprl Lemma : eqtt_to_assert 13,42

b:. (b = tt)  (b
latex


Upbool 1, bool 1
Definitions, t  T, P  Q, P  Q, P & Q, P  Q, x:AB(x), True, if b then t else f fi , b, tt, Unit, , False, A, ff,
Lemmasassert wf, btrue wf, bool wf, btrue neq bfalse, assert of ff

origin